k:Knd. (isrcv(k))  (lnk(k)  IdLnk) 

latex

Definitions	x:A. B(x), Knd, P  Q, isrcv(k), t  T, lnk(k), x. t(x), x(s), prop{i:l}
Lemmas	pi1 wf, IdLnk wf, Id wf, outl wf, assert wf, isl wf